\begin{tabbing}
abstract{-}chain{-}replication\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Rsp}$; ${\it isupdate}$; ${\it In}$; ${\it Out}$; ${\it Sys}$; $f$; ${\it Delta}$; $Q$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=fifo{-}antecedent(${\it es}$;${\it Sys}$;$f$)\+
\\[0ex]\& ($\forall$$u$:E(${\it Sys}$). ($f$($u$) = $u$) $\Leftarrow\!\Rightarrow$ ($\uparrow$($u$ $\in_{b}$ ${\it In}$)))
\\[0ex]\& (E(${\it In}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]\& (E(${\it Out}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]\& ($\forall$$e$:E(${\it In}$). ($\neg$($\uparrow$(${\it isupdate}$(${\it In}$($e$))))) $\Rightarrow$ ($\uparrow$($e$ $\in_{b}$ ${\it Out}$)))
\\[0ex]\& ($\forall$$e$:E(${\it Sys}$). ($\neg$($\uparrow$($e$ $\in_{b}$ ${\it In}$))) $\Rightarrow$ (loc($f$($e$)) = loc($e$)) $\Rightarrow$ ($\neg$($\uparrow$($e$ $\in_{b}$ ${\it Out}$))))
\\[0ex]\& input{-}forwarding\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Sys}$; ${\it isupdate}$; ${\it In}$; $f$)
\-\\[0ex]\& ($\exists$${\it chain}$:E(${\it Sys}$)$\rightarrow$(Id List). chain{-}consistent($f$;${\it chain}$))
\\[0ex]\& (\=$\forall$$e$:E(${\it Out}$).\+
\\[0ex](\=is{-}query(${\it In}$;${\it isupdate}$;$e$)\+
\\[0ex]$\Rightarrow$ (${\it Out}$($e$) = $Q$(filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; $e$)),${\it In}$($e$))))
\-\\[0ex]\& (\=($\neg$is{-}query(${\it In}$;${\it isupdate}$;$e$))\+
\\[0ex]$\Rightarrow$ (${\it Out}$($e$) = ${\it Delta}$(filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; $e$))))))
\-\-\-
\end{tabbing}